{-# OPTIONS --cubical=compatible --two-level #-}

open import Cubical-without-glue-Import.Without-glue -- requires at least @--cubical=no-glue@
